0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 22 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 UsableRulesProof (⇔, 0 ms)
↳8 PiDP
↳9 PiDPToQDPProof (⇒, 0 ms)
↳10 QDP
↳11 QDPSizeChangeProof (⇔, 0 ms)
↳12 YES
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_gag(X, s(Y), Z))
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gag(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gag(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
U1_gag(X, Y, Z, average_out_gag(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_gag(X, s(Y), Z))
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gag(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gag(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
U1_gag(X, Y, Z, average_out_gag(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
AVERAGE_IN_GAG(s(X), Y, Z) → U1_GAG(X, Y, Z, average_in_gag(X, s(Y), Z))
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_GAG(X, s(Y), Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → U2_GAG(X, Y, Z, average_in_gag(s(X), Y, Z))
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAG(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_gag(X, s(Y), Z))
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gag(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gag(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
U1_gag(X, Y, Z, average_out_gag(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
AVERAGE_IN_GAG(s(X), Y, Z) → U1_GAG(X, Y, Z, average_in_gag(X, s(Y), Z))
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_GAG(X, s(Y), Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → U2_GAG(X, Y, Z, average_in_gag(s(X), Y, Z))
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAG(s(X), Y, Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_gag(X, s(Y), Z))
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gag(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gag(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
U1_gag(X, Y, Z, average_out_gag(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAG(s(X), Y, Z)
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_GAG(X, s(Y), Z)
average_in_gag(0, 0, 0) → average_out_gag(0, 0, 0)
average_in_gag(0, s(0), 0) → average_out_gag(0, s(0), 0)
average_in_gag(0, s(s(0)), s(0)) → average_out_gag(0, s(s(0)), s(0))
average_in_gag(s(X), Y, Z) → U1_gag(X, Y, Z, average_in_gag(X, s(Y), Z))
average_in_gag(X, s(s(s(Y))), s(Z)) → U2_gag(X, Y, Z, average_in_gag(s(X), Y, Z))
U2_gag(X, Y, Z, average_out_gag(s(X), Y, Z)) → average_out_gag(X, s(s(s(Y))), s(Z))
U1_gag(X, Y, Z, average_out_gag(X, s(Y), Z)) → average_out_gag(s(X), Y, Z)
AVERAGE_IN_GAG(X, s(s(s(Y))), s(Z)) → AVERAGE_IN_GAG(s(X), Y, Z)
AVERAGE_IN_GAG(s(X), Y, Z) → AVERAGE_IN_GAG(X, s(Y), Z)
AVERAGE_IN_GAG(X, s(Z)) → AVERAGE_IN_GAG(s(X), Z)
AVERAGE_IN_GAG(s(X), Z) → AVERAGE_IN_GAG(X, Z)
From the DPs we obtained the following set of size-change graphs: